\begin{tabbing}
locl($a$) sends [${\it tg}$,$f$\{$A$$\rightarrow$$T$\}($x$)] on link $l$ once
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=vartype(source($l$);$x$) $\subseteq\rho$ $A$ \& ($\forall$$e$:E. kind($e$) $=$ rcv($l$,${\it tg}$) $\Rightarrow$ valtype($e$) $\subseteq\rho$ $T$)\+
\\[0ex]\& (\=$\exists$$e$:E.\+
\\[0ex]kind($e$) $=$ rcv($l$,${\it tg}$)
\\[0ex]\& \=val($e$) $=$ $f$($x$ when sender($e$))\+
\\[0ex]\& kind(sender($e$)) $=$ locl($a$)
\\[0ex]\& ($\forall$${\it e'}$:E. kind(${\it e'}$) $=$ rcv($l$,${\it tg}$) $\Rightarrow$ kind(sender(${\it e'}$)) $=$ locl($a$) $\Rightarrow$ ${\it e'}$ $=$ $e$))
\-\-\-
\end{tabbing}